00100	GIVEAX(EQ1,(∀ X)(X=X));
00200	
00300	GIVEAX(EQ2,(∀ X)(∀ Y)(X=Y ⊃ Y=X));
00400	
00500	GIVEAX(EQ3,(∀ X)(∀ Y)(∀ Z)(X=Y ∧ Y=Z ⊃ X=Z));
00600	
00700	GIVEAX(TABLEEMPTY,(∀ X)(¬(X=ROBOT)∧¬HOLDING(X,S0)⊃¬AT(X,TABLE,S0)));
00800	
00900	GIVEAX(DIFFOBJ,¬(BOX1=BOX2)∧(¬(BOX1=TABLE)∧(¬(BOX1=DOOR)∧
01000	(¬(BOX1=OUTSIDE)∧(¬(BOX2=TABLE)∧(¬(BOX2=DOOR)∧(¬(BOX2=OUTSIDE)∧
01100	(¬(TABLE=DOOR)∧(¬(TABLE=OUTSIDE)∧¬(DOOR=OUTSIDE))))))))));
01200	
01300	GIVEAX(ATONE,(∀ X)(∀ P1)(∀ P2)(∀ S)(AT(X,P1,S)∧AT(X,P2,S)⊃(P1=P2)));
01400	
01500	GIVEAX(REDDOOR,(∃ X)(RED(X)∧(¬(X=ROBOT)∧(AT(X,DOOR,S0)∧
01600	(∀ Y) (AT(Y,DOOR,S0)∧(¬(Y=ROBOT)∧¬HOLDING(Y,S0))⊃RED(Y))))));
01700	
01800	GIVEAX(ISKEYBOX,KEYBOX=BOX1∨KEYBOX=BOX2);
01900	
02000	GIVEAX(KEYBOX1,(∃ X)(KEY(X)∧(¬(X=ROBOT)∧(AT(X,KEYBOX,S0)
02100	∧¬HOLDING(X,S0)))));
02200	GIVEAX(KEYBOX2,(∀ Y) (AT(Y,KEYBOX,S0)
02300	∧(¬(Y=ROBOT)∧¬HOLDING(Y,S0))⊃KEY(Y)));
02400	
02500	
02600	GIVEAX(B1B2,¬(BOX1=BOX2));
02700	GIVEAX(B1T,¬(BOX1=TABLE));
02800	GIVEAX(B1D,¬(BOX1=DOOR));
02900	GIVEAX(B1O,¬(BOX1=OUTSIDE));
03000	GIVEAX(B2T,¬(BOX2=TABLE));
03100	GIVEAX(B2D,¬(BOX2=DOOR));
03200	GIVEAX(B2O,¬(BOX2=OUTSIDE));
03300	GIVEAX(TD,¬(TABLE=DOOR));
03400	GIVEAX(TO,¬(TABLE=OUTSIDE));
03500	GIVEAX(DO,¬(DOOR=OUTSIDE));
03600	
03700	GIVEAX(HOLDING,(∀ S)(∀ X)(∀ Y)(AT(ROBOT,Y,S)∧HOLDING(X,S)⊃
03800		AT(X,Y,S)));
03900	
04000	GIVEAX(HOLD2,(∀ S)(∀ X)(∀ Y)(HOLDING(X,S)∧HOLDING(Y,S)
04100		⊃(X=Y)));
04200	
04300	GIVEAX(PICKUP,(∀ S)((LAMBDA SP)((∀ X)(∀ Y)(AT(X,Y,S)≡AT(X,Y,SP)))∧
04400	((∀ Z)(AT(ROBOT,Z,S)
04500	∧(∃ X)(¬(X=ROBOT)∧AT(X,Z,S))⊃(∃X)(HOLDING(X,SP)))))(PICKUP(S)));
04600	
04700	GIVEAX(GO1,(∀ S)(∀ Z)(∀ W)(HOLDING(W,S)≡HOLDING(W,GOO(Z,S))));
04800	
04900	GIVEAX(GO2,(∀ S)(∀ Z)(¬(Z=OUTSIDE)∨(∃ X)(AT(X,DOOR,S)∧KEY(X))
05000		⊃ AT(ROBOT,Z,GOO(Z,S))));
05100	
05200	GIVEAX(GO3,(∀ S)(∀ Z)(∀ X)(∀ Y)(AT(X,Y,S)∧(¬(X=ROBOT)∧¬HOLDING(X,S))
05300		⊃AT(X,Y,GOO(Z,S))));
05400	
05500	GIVEAX(GO4,(∀ S)(∀ Y)((∀ X)(¬(AT(X,DOOR,S)∧KEY(X))))∧
05600		AT(ROBOT,Y,S)
05700		⊃AT(ROBOT,Y,GOO(OUTSIDE,S)));
05800	
05900	GIVEAX(GO5,(∀ S)(∀ Z)(∀ X)(∀ Y)(¬(X=ROBOT)∧(¬HOLDING(X,S)
06000	∧AT(X,Y,GOO(Z,S)))⊃AT(X,Y,S)));
06100	
06200	GIVEAX(RELEASE1,(∀ S)(∀ X)(∀ Y)(AT(X,Y,S)≡AT(X,Y,RELEASE(S))));
06300	
06400	GIVEAX(RELEASE2,(∀ S)(∀ X)(¬HOLDING(X,RELEASE(S))));
06500	
06600	END;